$\forall$$T$:Type, $L$:$T$ List, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$). ($L$ o $f$) $\in$ $T$ List